/*
 * FindFails.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include <cassert>

#include <iostream>
#include <fstream>
#include <utility>
#include <string>

#include "bfr/Clause.hpp"
#include "bfr/Literal.hpp"

#include "bfr/ClauseSet.hpp"
#include "bfr/OccurrencePattern.hpp"

#include "bfr/DIMACSParser.hpp"
#include "bfr/DIMACSCollectionParser.hpp"

#include "bfr/CoefficientType.hpp"
#include "bfr/LPB.hpp"
#include "bfr/LPBConversionException.hpp"

#include "bfr/lpbCombinatorial/SolverInformation.hpp"
#include "bfr/lpbCombinatorial/SplittingTreeNode.hpp"
#include "bfr/lpbCombinatorial/SplittingTree.hpp"
#include "bfr/lpbCombinatorial/MinimumChooser.hpp"

#include "bfr/lpbCombinatorial/TreeToLPB.hpp"

using namespace std;
using namespace bfr;

bool runMinSolver(TreeToLPB<MinimumChooser> &minSolver, size_t size,
                      ClauseSet *cs, bool cutTree) {
    double result = 0;
    // start combinatorial solver
    SplittingTree t(cs, size);
    if (cutTree) {
        t.createTree<true>(true, false);
    }
    else {
        t.createTree<false>(true, false);
    }
    try {
        LPB *lpb = minSolver.solve(&t);
        // lpb->sortCoefficients();
        delete lpb;
        return true;
    } catch (const LPBConversionException &e) {
        return false;
    }
    assert(false);
    return true;
}

// finds all DNFs from a given DIMACS collection where the combinatorial
// algorithms in its normal mode fails
// not really some error handling here...
int main(int argc, char **argv) {
    if (argc != 5) {
        cerr << "Usage: " << argv[0] << " meta_in problem_in out cut" << endl;
        return 1;
    }
    bool cutTree = false;
    ifstream in;
    in.open(argv[2]);
    ifstream metaIn;
    metaIn.open(argv[1]);
    ofstream out;
    out.open(argv[3]);
    size_t num;
    metaIn >> num;
    string cutStr = argv[4];
    if ((cutStr == "true") || (cutStr == "1")) {
        cutTree = true;
    }
    DIMACSCollectionParser parser(&in, num);
    TreeToLPB<MinimumChooser> minSolver;
    for (DIMACSCollectionParser::const_iterator dit = parser.begin();
         dit < parser.end();
         dit++) {
        pair<ClauseSet*, size_t> next = *dit;
        if (!(runMinSolver(minSolver, next.second, next.first, cutTree))) {
            next.first->writeDIMACS(out);
        }
    }
    in.close();
    metaIn.close();
    out.close();
}
